#ifndef TERN_UTIL_H
#define TERN_UTIL_H

#include<stdio.h>
#include<pthread.h>
#include<tern/TernDefs.h>

namespace klee {
	class TernUtil {
	public:
		static inline atomic_t atomicInc(atomic_t *v) {
			return __sync_add_and_fetch(v, 1);
		}

		static inline atomic_t atomicDec(atomic_t *v) {
			return __sync_sub_and_fetch(v, 1);
		}

		static inline atomic_t atomicRead(atomic_t *v) {
			return __sync_add_and_fetch(v, 0);
			//return *v;
		}

		static inline void atomicSet(atomic_t *v, atomic_t newVal) {
			__sync_bool_compare_and_swap(v, *v, newVal);
		}

		static inline bool mutexAvailable(pthread_mutex_t *mutex) {
			if (pthread_mutex_trylock(mutex) != 0)
				return false;
 			else {
				pthread_mutex_unlock(mutex);
				return true;
			}	
		}

		static inline bool elementNotInVector(std::vector<unsigned> &v, unsigned element) {
			for (unsigned i = 0; i < v.size(); i++) {
				if (v[i] == element)
					return false;
			}
			return true;
		}

		static inline void delElementFromVector(std::vector<unsigned> &v, unsigned element) {
			assert(!elementNotInVector(v, element));
			for (unsigned i = 0; i < v.size(); i++) {
				if (v[i] == element) {
					v.erase(v.begin()+i);
					break;
				}
			}
			assert(elementNotInVector(v, element));
		}

		static inline void delElementFromVector(std::vector<int> &v, int element) {
			assert(!elementNotInVector(v, element));
			for (unsigned i = 0; i < v.size(); i++) {
				if (v[i] == element) {
					v.erase(v.begin()+i);
					break;
				}
			}
			assert(elementNotInVector(v, element));
		}
		
		static inline bool elementNotInVector(std::vector<int> &v, int element) {
			for (unsigned i = 0; i < v.size(); i++) {
				if (v[i] == element)
					return false;
			}
			return true;
		}
	
	};
}

#define forall(type, it, c) for(type::iterator it = (c).begin(); \
                                (it) != (c).end(); ++(it))

#define forit(it,c) for((it) = (c).begin(); (it) != (c).end(); ++(it))

#define fori(i,c) for((i) = 0; (i) < (int)(c).size(); ++(i))

#endif

